Lambda Calculus

Untyped Lambda Calculus

• :
  • start with a (infinite) set of variables \(\mathcal{V} = {a, b, c, ...}\)
  • \(\lambda\)-Calculus is a set of terms formed according to these three rules
    • 1. naming :: if \(x \in \mathcal{V}\), then \(x\) is a term in the \(\lambda\)-Calculus
    • 2. abstraction :: if \(T\) is a term and \(x \in \mathcal{V}\), then \(\lambda x. T\) is a term
    • 3. application :: if \(T_1\) and \(T_2\) are terms, then \(T_1 T_2\) is a term
• it's a model for general computation
• application and term rewriting:
  • for \(T_1 T_2\), when \(T_1\) is an abstraction, we allow re-write applications by substituting \(T_2\) for \(x\) through \(T_1\)
  • eg for abstraction select-first, \(\lambda x. \lambda y. x\), its application is like
    • \((\lambda x. \lambda y. x\ a)\ b \to\)
    • \((\lambda y. a)\ b \to\)
    • \(a\)
• eg: make-pair \(\lambda x. \lambda y. \lambda z\ ((z\ x)\ y)\)
  • when applies to \(a\) and \(b\)
  • we got: \(\lambda z\ ((z\ a)\ b)\)
  • its a term that encodes \(a\) and \(b\)
  • it expects an abstraction
• Alpha Equivalence: free and bound variables
  • : bound variables are "placeholders" that can be re-named at will without changing the essential meaning of a term.
  • in a term, there are 3 categories of variable occurrences
    • 1. binding: on the left side of \(.\) in an abstraction
    • 2. bound
    • 3. free: in \(\lambda x. M\), \(x\) is bound in \(M\)
  • rules: ...
  • it allows \(\lambda x. (x\ \lambda x. x)\ y\) to make sense: inner \(x\) and outer \(x\) are different
  • the operation of renaming: \(M^{x \to y}\) denotes the result of replacing every free occurrence of \(x\) in \(M\) with \(y\)
• Beta Reduction
  • : the process of applying a function (an abstraction) to an argument (another term)
  • \((\lambda x. M)\ N\) is called a redex (reducible expression)
  • rule
    • : substitute every occurrence of the bound variable \(x\) inside the function body \(M\) with the argument \(N\)
    • notation for substitution: \(M[x := N]\)
    • the rule can be written as \((\lambda x. M)\ N \to_{\beta} M[x := N]\)
• \(\beta\)-normal: when is \(\beta\)-reduction done?
  • We say that a term \(M\) is in \(\beta\)-normal form (\(\beta\)-nf) if \(M\) contains no redex, ie, there's no way to perform beta-reduction to reduce it to a simpler form

Simply Typed Lambda Calculus \(\lambda_{\to}\)

• :
  • in addition to ordinary variables \(\mathcal{V}\) in untyped lambda calculus, we now have another set of type variables \(\mathbb{V} = {\alpha, \beta, \gamma, ...}\), and we can define the set of all simple types \(\mathbb{T}\) as:
    • 1. if \(\alpha \in \mathbb{V}\), then \(\alpha \in \mathbb{T}\)
    • 2. if \(\alpha, \tau \in \mathbb{V}\), then \(\alpha \to \tau \in \mathbb{T}\)
  • we write \(M: \sigma\) for "term \(M\) has type \(\sigma\)"
  • we assume each ordinary variable has an unique type
  • we denote abstraction more fully as \(\lambda x: \sigma. M: \sigma \to \tau\)
• context: a collection of type statements \(x: \sigma\), \(y: \tau\), \(z: \upsilon\)
• judgement: a statement \(\Gamma \vdash M: \sigma\), where they are a context, a term, and a type respectively
• derivation
  • : we can validate a judgement by derivation
  • 3 derivation rules
    • 1. var: \(\Gamma \vdash x : \sigma\) if \(x : \sigma \in \Gamma\)
    • 2. appl: \(\frac{\Gamma \vdash M: \sigma \to \tau \Gamma \vdash N: \sigma}{\Gamma \vdash MN : \tau}\)
    • 3. abst: \(\frac{\Gamma, x: \sigma \vdash M : \tau}{\Gamma \vdash \lambda x: \sigma. M: \sigma \to \tau}\)
  • Each rule tells us what we can conclude so long as we know certain things
  • A derivation is collection of applications of these rules, arranged in an inverted tree where the "root", at the bottom, is the statement we are justifying.
• Questions we can ask now:
  • 1. well-typedness / typability: given a term, is it legal in some context?
  • 2. type checking: given a judgement, is it true?
  • 3. term finding: is there a term of the given type in the given context?
    • previous 2 are decidable, this one is undecidable
    • under Curry-Howard, term finding is equivalent to proof finding
• We can now rule out misbehaving terms. All terms are strongly normalizing as their reduction to normal form is guaranteed to terminate.
  • downside: it's not very expressive

Second-order Lambda Calculus - \(\lambda 2\) - Polymorphic Lambda Calculus - System F

• All above names are referring to the same thing
• \(\land\)

Reference

• https://www.unwoundstack.com/blog/the-lambda-calculus.html
• https://www.unwoundstack.com/blog/the-simply-typed-lambda-calculus.html